Leslie Lamport

概述

美国计算机科学家（1941–），分布式系统理论的奠基者，2013年 ACM 图灵奖得主。发明了逻辑时钟、拜占庭将军问题、Paxos 共识协议和 TLA+ 规约语言。

关键内容

逻辑时钟（1978）

• 定义了 happened-before 偏序关系
• 发明了逻辑时钟机制
• 给出了分布式互斥算法
• 论文仅8页，被引超过14,000次

拜占庭将军问题（1982）

• 形式化了分布式系统中的容错问题
• 提出了拜占庭容错（BFT）的概念

Paxos 共识协议（1989/1998）

• 解决了分布式共识问题
• 成为现代分布式系统的核心组件

TLA+

• 高级规约语言，用于描述和验证并发和分布式系统

图灵奖（2013）

授奖理由是"对分布式和并发系统的理论与实践做出的根本性贡献"。

写作风格

Lamport 以其清晰、简洁、精确的技术写作而广受赞誉。他的论文被视为分布式系统论文写作的典范。

来源

• raw/books/计算机科学/13-lamport-time-clocks.md

相关

• Lamport 逻辑时钟论文 — 1978年发表
• 逻辑时钟 — 发明
• happened-before 关系 — 定义
• 分布式系统 — 理论奠基
• Paxos — 共识协议
• 拜占庭将军问题 — 1982年提出
• 向量时钟 — 后续发展
• 分布式互斥算法 — 提出